A:Type, eq:EqDecider(A), B:(AType), P:(x:AB(x)), x:A, v:B(x).
ydom(x : v). w=x : v(y)   P(y,w)  P(x,v) 

latex

Definitions	b, f(x), x : v, x  dom(f), xdom(f). v=f(x)   P(x;v), t  T, x:A. B(x), EqDecider(T), , x(s), x(s1,s2), ff, eqof(d), p q, P  Q, P  Q, P & Q, P  Q, True, False, P  Q
Lemmas	subtype rel self, assert of bor, deq property, eqof eq btrue, assert wf, bor wf, eqof wf, bfalse wf, deq wf